Nuprl Lemma : divides_functionality_wrt_assoced
11,40
postcript
pdf
a
,
a'
,
b
,
b'
:
. assoced(
a
;
a'
)
assoced(
b
;
b'
)
(divides(
a
;
b
)
divides(
a'
;
b'
))
latex
Definitions
prop{i:l}
,
t
T
,
P
Q
,
P
Q
,
P
Q
,
assoced(
a
;
b
)
,
P
Q
,
x
:
A
.
B
(
x
)
Lemmas
divides
wf
,
divides
transitivity
origin
a,a',b,b':
. assoced(a; a') 
assoced(b; b') (divides(a; b) 
divides(a'; b')) a,a',b,b':. assoced(a; a') assoced(b; b') (divides(a; b) divides(a'; b')) 
T Q
Q Q Qx:A. B(x)